choose(n;i) == if (i = 0) (i = n) then 1 else choose(n - 1;i - 1)+choose(n - 1;i) fi 
(recursive) 

latex

Up	rings 1
Wellformedness Lemmas	choose wf
Definitions	Y, if b then t else f fi , p q, (i = j)